\chapter{Formal Analysis}
\label{cap:Formal Analysis}
\section{Introduction}
This appendix is supposed to provide a formal requirements analysis by using alloy language.
First of all a class diagram, representing the general system, is provided. According to this class diagram and the previous requirements shown in this document, we use alloy in order to make static and dynamic model.
\newpage
\section{Model Description}
\noindent
The attached class diagram is an approximate one. Its purpose is to provide an high level idea of the system but it does not concern with the implementation. By the way it could well represent the entities of the Alloy model we are going to provide. \\
\begin{center}
\begin{figure}[h]
        \includegraphics[scale=0.55]{images/ClassDiagram}
        \caption{Class Diagram}
\end{figure}
\end{center}
\noindent
In this Diagram there are only relations between entities of the system, the dynamic behavior is not shown, because it's well described by the use case description and sequence diagrams in the previous part of this document.
\newpage
\section{Alloy Code}

\lstset{language=Alloy, breaklines=true, breakatwhitespace=false}

\lstinputlisting[label=StaticModel, caption=Static Model]{../Alloy/SWIMv2_Model.als}
\clearpage
\lstinputlisting[label=DynamicModel, caption=Dynamic Model]{../Alloy/SWIMv2_DynamicModel.als}
\clearpage
\lstinputlisting[label=TimeLibrary, caption=Time Library]{../Alloy/time.als}

\newpage
\section{Analysis Result}
\subsection*{Static Model}
First of all Two screenshoots of our static Model:
\\
In this world, the admin ask for the help of the Founder in day 2. The help Request will expire the day after. In day 4 the admin leaves the Founder a feedback.
\\
\begin{figure}[!ht]
	\centering
        \includegraphics[scale=0.8]{images/alloyModels/ex2_feedback}
        \caption{Alloy Static Model - Feedbacks}
\end{figure}

In this world, projected over the bool ``true'',  we can see a guest, that is never logged, the Founder, that in day 0 is not logged, and a registered user, always logged.
\\

\begin{figure}[!ht]
	\centering
        \includegraphics[scale=0.8]{images/alloyModels/ex3_login}
        \caption{Alloy Static Model - Login}
\end{figure}



\clearpage
\subsection*{Dynamic Model}
We show here some screen-shots of our dynamic Alloy model, we projected on the State class.
\\
In State 0, the current day (Today label) is 0 and there are a Founder and a Registered User. The registered user send himself a message.

\begin{figure}[!ht]
	\centering
        \includegraphics[scale=0.8]{images/alloyModels/ex1_state_0}
        \caption{Alloy Model - Projection on State 0}
\end{figure}

In state 1, the curent day is 1, the registered User has been banned and the founder send him a message.

\begin{figure}[!ht]
	\centering
        \includegraphics[scale=0.8]{images/alloyModels/ex1_state_1}
        \caption{Alloy Dynamic Model - Projection on State 1}
\end{figure}

In state 2, the current day is 2, the ban has finished and the founder send a message to himself.


\begin{figure}[!ht]
	\centering
        \includegraphics[scale=0.8]{images/alloyModels/ex1_state_2}
        \caption{Alloy Dynamic Model - Projection on State 2}
\end{figure}

No constraints neither in this RASD nor in the Alloy model forbid registered users to send messages themselves.




